#include <stdio.h>

/*插入排序*/

#define LEN 5
int a[LEN] = { 10, 5, 2, 4, 7 };

void insertion_sort(void)
{
	int i, j, key;
	for (j = 1; j < LEN; ++j) {
		printf("%d, %d, %d, %d, %d\n", a[0], a[1], a[2], a[3], a[4]);
		key = a[j];
		i = j - 1;
		while (i >= 0 && a[i] > key) {
			a[i+1] = a[i];
			--i;
		}
		a[i+1] = key;
	}
	printf("%d, %d, %d, %d, %d\n", a[0], a[1], a[2], a[3], a[4]);
}

int main(void)
{
	insertion_sort();
	return 0;
}

/*
10, 5, 2, 4, 7
5, 10, 2, 4, 7
2, 5, 10, 4, 7
2, 4, 5, 10, 7
2, 4, 5, 7, 10

如何严格证明这个算法是正确的？
换句话说，只要反复执行该算法的for循环体，执行LEN-1次，就一定能把数组a排好序，而不管数组a的原始数据是什么，如何证明这一点呢？
可以借助Loop Invariant的概念和数学归纳法来理解循环结构的算法，
假如某个判断条件满足以下三条准则，它就称为Loop Invariant：
1.第一次执行循环体之前该判断条件为真
2.如果“第N-1次循环之后（或者说第N次循环之前）该判断条件为真”这个前提可以成立，那么就有办法证明第N次循环之后该判断条件仍为真
3.如果在所有循环结束后该判断条件为真，那么就有办法证明该算法正确地解决了问题
只要找到了这个Loop Invariant，就可以证明一个循环结构的算法是正确的。
上面插入排序算法的Loop Invariant是这样的判断条件：第j次循环之前，子序列a[0..j-1]是排好序的。

第一条就相当于递归的Base Case，第二条就相当于递归的递推关系。这再次说明了递归和循环是等价的
*/
